$\forall$${\it es}$:event\_system\{i:l\}, $e$:es{-}E(${\it es}$), $l$:IdLnk, $L$:(es{-}E(${\it es}$) List).
\\[0ex]es{-}rcv{-}from(${\it es}$; $e$; $l$; $L$) $\Rightarrow$ (es{-}receives(${\it es}$; $e$; $l$) = $L$)